COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnify{1100}
C00013 00003	\def\Lemma:{\par\noindent{\bf Lemma:}\quad}
C00015 00004	\prob {1.1}.
C00020 00005	\prob{1.2}. The functions |istail| and |commontail| are defined as:
C00023 00006	\prob{1.4}. This turned out to be one of the hardest problems.  Here is a fairly
C00030 00007	\prob {1.5}. [The following solution is by Oliver Buckley.]  First, define
C00032 00008	\prob{2.1}.  First we have to write the functions |get| and |point|.
C00037 ENDMK
C⊗;
\magnify{1100}
\font\tt=cmsa10
\catcode`|=13
\def|#1|{\hbox{\it#1\/}}
\parindent 0pt
\parskip 0pt
\def\pskip{\penalty-1000\vskip 6pt plus 2pt minus 1pt}
\def\ppskip{\penalty-2000\vskip 10pt plus 3pt minus 2pt}
\def\prob#1.{\par\noindent Problem #1.\quad\ignorespace}
\def\no(#1){\noindent\hbox to 6em{(#1)\hfill}}
\catcode`⊗=13
\def⊗{\hbox to 2em{}}
\def\IF{\mathop{\bf if}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}
\def\AND{\mathrel{\bf and}}
\def\OR{\mathrel{\bf or}}
\def\NOT{\mathop{\bf not}}
\def\N{\mathop{\bf n}}
\def\T{\hbox{\tt T}}
\def\NIL{\hbox{\tt NIL}}
\def\.{\mathbin{.}}
\def\A{\mathop{\bf a}}
\def\D{\mathop{\bf d}}
\def\EQ{\mathrel{\bf eq}}
\def\AT{\mathop{\bf at}}
\def\quote#1{\hbox{\sfcode`.=1000\tt#1}}
\def\list#1{\langle#1\rangle}

{\catcode`\↑↑M=13\global\let ↑↑M=\linebreak}	% This must be on one line!
\def\lines{\par\groupbegin
	\catcode`\ =12
	\sfcode`.=1000
	\parindent 0pt
	\leftskip 25pt
	\rightskip 0pt plus 1fil
	\interlinepenalty 50
	\baselineskip 12pt
	\parskip 12pt plus 6pt minus 6pt
	\catcode`\↑↑M=13
	\tt\eat}
\def\eat#1{}					% to eat the first <cr>
\def\endlines{\par\vskip\minusthe\baselineskip	% cancel the last empty line
	\vskip\the\parskip			% put in space
	\groupend\vskip\minusthe\parskip}	% cancel the next space to go in

\ctrline{CS 206---Recursive Programming and Proving}
\ctrline{Homework 2 Solutions}
\ctrline{Tuesday, December 7, 1982}

\ppskip
{\bf Grading}:
Problems 3--7 and 9--11 received 3 points each, because they had been solved
in the previous assignment.  Problem 8 got 6 points because it was longer.
Each part of problem 20 and of problem 22 was worth 10 points.  This adds up
to 100 points.

\pskip
{\bf Solutions}:
The solutions for problems 3--11 in external form have been handed out already.
Translation into MacLisp internal form is straightforward.

\ppskip
\prob 20.
One problem encountered was what to do when one of the input polynomials
is \NIL.  The natural mathematical meaning of \NIL\ is the 0 polynomial, and
allowing this simplifies most programs.  It does work, though, to disallow \NIL\
and use \quote{(0)} to represent 0.
\pskip
\no(a)$|sum|[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\THEN v$\par
$⊗⊗⊗⊗\ELSE\IF\N v\THEN u$\par
$⊗⊗⊗⊗\ELSE(\A u+\A v)\.|sum|[\D u,\D v]$\par
\pskip
\lines
(defun sum (u v)
       (cond ((null u) v)
             ((null v) u)
             (t (cons (plus (car u) (car v))
                      (sum (cdr u) (cdr v))))))
\endlines

\ppskip
\no(b)$|prod|[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE|sum|[|prod|[\D u,0\.v],|scalarprod|[\A u,v]]$\par
\pskip
$⊗⊗⊗|scalarprod|[x,v]←$\par
$⊗⊗⊗⊗\IF\N v\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE (x\times\A v)\.|scalarprod|[x,\D v]$\par
\pskip
\lines
(defun prod (u v)
       (cond ((null u) nil)
             (t (sum (prod (cdr u) (cons 0 v))
                     (scalarprod (car u) v)))))

(defun scalarprod (x v)
       (cond ((null v) nil)
             (t (cons (times x (car v))
                      (scalarprod x (cdr v))))))
\endlines
\pskip
The |scalarprod| function could be made part of |prod|, by using |mapcar|
and a $λ$-expression, but it will be useful to have it for later functions.

\ppskip
\no(c)$|quot|[u,v]←|reverse|\,|quot1|[|stripz|\,|reverse|\,u,
|stripz|\,|reverse|\,v]$\par
\pskip
$⊗⊗⊗|stripz|\,u←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE\IF\A u=0\THEN|stripz|\,\D u$\par
$⊗⊗⊗⊗\ELSE u$\par
\pskip
$⊗⊗⊗|quot1|[u,v]←$\par
$⊗⊗⊗⊗\IF\N v\THEN\quote{ERROR}$\par
$⊗⊗⊗⊗\ELSE\IF|length|\,u<|length|\,v\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE (\A u\div\A v)\.|quot1|[|sum|[\D u,|scalarprod|[-(\A u\div\A v),\D v]],v]$\par
\pskip
\lines
(defun quot (u v)
       (reverse (quot1 (stripz (reverse u))
                       (stripz (reverse v)))))

(defun stripz (u)
       (cond ((null u) nil)
             ((zerop (car u)) (stripz (cdr u)))
             (t u)))

(defun quot1 (u v)
       (cond ((null v) 'error)
             ((lessp (length u) (length v)) nil)
             (t (cons (quotient (float (car u)) (car v))
                      (quot1 (sum (cdr u)
                                  (scalarprod
                                   (minus (quotient (float (car u))
                                                    (car v)))
                                   (cdr v)))
                             v)))))
\endlines
\pskip
To divide polynomials, we need to access the highest-powered coefficients
most often.  Therefore, it seems easiest to reverse both polynomials first
and reverse the result at the end.  The |stripz| function is used to prevent
division by zero terms which may appear in $v$.  To ensure the the division
is done in floating point, we convert $\A u$ to a flonum before dividing.

\ppskip
\no(d)$|rem|[u,v]←|sum|[u,-|prod|[quot[u,v],v]]$\par
\pskip
\lines
(defun rem (u v)
       (sum u
            (mapcar (function minus)
                    (prod (quot u v) v))))
\endlines

\ppskip
\prob 22. In the following solutions, we will assume that there are no
repetitions of elements in the lists that are input, and produce output
lists with no repititions.
\pskip
\no(a)$|union|[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\THEN v$\par
$⊗⊗⊗⊗\ELSE\IF|member|[\A u,v]\THEN|union|[\D u,v]$\par
$⊗⊗⊗⊗\ELSE\A u\.|union|[\D u,v]$\par
\pskip
\lines
(defun union (u v)
       (cond ((null u) v)
             ((member (car u) v) (union (cdr u) v))
             (t (union (cdr u) v))))
\endlines

\ppskip
\no(b)$|inter|[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE\IF|member|[\A u,v]\THEN\A u\.|inter|[\D u,v]$\par
$⊗⊗⊗⊗\ELSE|inter|[\D u,v]$\par
\pskip
\lines
(defun inter (u v)
       (cond ((null u) nil)
             ((member (car u) v) (cons (car u) (inter (cdr u v))))
             (t (inter (cdr u) v))))
\endlines

\ppskip
\no(c)$|diff|[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE\IF|member|[\A u,v]\THEN|diff|[\D u,v]$\par
$⊗⊗⊗⊗\ELSE\A u\.|diff|[\D u,v]$\par
\pskip
\lines
(defun diff (u v)
       (cond ((null u) nil)
             ((member (car u) v) (diff (cdr u) v))
             (t (cons (car u) (diff (cdr u) v)))))
\endlines

\vfill\eject
\def\Lemma:{\par\noindent{\bf Lemma:}\quad}
\def\Theorem:{\par\noindent{\bf Theorem:}\quad}
\def\Proof:{\par\noindent{\bf Proof:}\quad}
\def\samelength{\mathop{\it samelength}}
\def\reverse{\mathop{\it reverse}}
\def\length{\mathop{\it length}}
\def\istail{\mathop{\it istail}}
\def\com{\mathop{\it commontail}}
\def\upto{\mathop{\it upto}}
\def\get{\mathop{\it get}}
\def\point{\mathop{\it point}}

\ctrline{Homework 3 Solutions}

\ppskip
{\bf Grading}:
Each problem received 10 points.  Thus there were 80 points altogether.

\ppskip
{\bf Solutions}:
Answers to all except problem 2.2 are given.  That one is missing because
I didn't have the time to write up a solution.

\ppskip
\prob {1.1}.
There were two basic approaches to solving this problem, differing
in whether the formula $∀u.\,\samelength[u,\reverse u]$ was proved directly
or whether |length| was used as an auxiliary function.  The functions used
are defined as follows:
\pskip
$⊗⊗⊗\reverse u←\IF\N u\THEN\NIL\ELSE\reverse[\D u]*\list{\A u}$\par
\pskip
$⊗⊗⊗\samelength[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\OR\N v\THEN\N u\AND\N v$\par
$⊗⊗⊗⊗\ELSE\samelength[\D u,\D v]$\par
\pskip
$⊗⊗⊗\length u←\IF\N u\THEN 0\ELSE 1+\length \D u$\par
\pskip
\noindent Here is a direct proof (courtesy of Keith Hall):
\pskip
\Lemma: $∀x\,u\,v.\,\samelength[u,v*\list{x}]≡\samelength[u,x\.v]$.
\Proof: We will prove the lemma by list induction on $\Phi(v)$:
$∀x\,u.\,\samelength[u,v*\list{x}]≡\samelength[u,x\.v]$.
First, $\Phi(\NIL)$ is $∀x\,u.\,\samelength[u,\list{x}]≡
\samelength[u,x\.\NIL]$ (expanding the |append| on the left-hand side),
which is valid since $\list{x}=x\.\NIL$ for any $x$.
Now, assume $\Phi(v)$ as an inductive hypothesis; then $\Phi(y\.v)$ is
$∀x\,u.\,\samelength[u,(y\.v)*\list{x}]≡\samelength[u,x\.(y\.v)]$.
If $u=\NIL$, both sides of the equivalence are \NIL\ using the definition
of |samelength| and facts about |cons| and |append|; and if $u≠\NIL$,
the formula simplifies to $\samelength[\D u,v*\list{x}]≡\samelength[\D u,y\.v]$.
Using the inductive hypothesis, this is the same as
$\samelength[\D u,x\.v]≡\samelength[\D u,y\.v]$, but here again the second
argument to both calls of |samelength| is non-\NIL; so either $\D u=\NIL$ and
both sides are false, or $\D u≠\NIL$ and then the formula becomes
$\samelength[\D\D u,v]≡\samelength[\D\D u,v]$, which is valid.
\pskip
\Theorem: $∀u.\,\samelength[u,\reverse u]$.
\Proof: By induction on $\Phi(u)$: $\samelength[u,\reverse u]$.
$\Phi(\NIL)$ is trivial (apply the definitions of |reverse| and |samelength|).
Assuming $\Phi(u)$, $\Phi(x\.u)$ is
\pskip
$⊗⊗⊗\samelength[x\.u,\reverse [x\.u]]$\par
$⊗⊗⊗⊗≡\samelength[x\.u,\reverse u*\list{x}]$\par
$⊗⊗⊗⊗≡\samelength[x\.u,x\.\reverse u]$\hskip 3em (by the lemma)\par
$⊗⊗⊗⊗≡\samelength[u,\reverse u]$\par
\pskip
and the last line is true by the inductive hypothesis.

\ppskip
A proof using |length| as an auxiliary function would prove the following
lemmas, from which the main result follows.
\pskip
\Lemma: $∀u\,v.\,\samelength[u,v]≡\length u=\length v$.
\Lemma: $∀u\,v.\,\length[u*v]=\length u+\length v$.
\pskip
Both of these can be proved by list induction on $u$ or $v$ (or both).

\ppskip
\prob{1.2}. The functions |istail| and |commontail| are defined as:
\pskip
$⊗⊗⊗\istail[u,v]←u=v\OR[\NOT\N v\AND\istail[u,\D v]]$\par
\pskip
$⊗⊗⊗\com[u,v]←\IF\istail[u,v]\THEN u\ELSE\com[\D u,v]$\par
\pskip
Let $\Phi(u)$ be $\istail[\com[u,v],v]$.  Then $\Phi(\NIL)$ is
seen to be true by applying the function definitions, and assuming $\Phi(u)$,
$\Phi(x\.u)$ is
\pskip
$⊗⊗⊗\istail[\com[x\.u,v],v]$\par
$⊗⊗⊗⊗≡\istail[\IF\istail[x\.u,v]\THEN x\.u\ELSE\com[u,v],v]$\par
$⊗⊗⊗⊗≡\IF\istail[x\.u,v]\THEN\istail[x\.u,v]\ELSE\istail[\com[u,v],v]$\par
\pskip
which is valid, applying the inductive hypothesis.  Since no assumptions were
made about $x$, we can quantify over $x$, completing the inductive step.

\ppskip
\prob{1.3}. Let $\Phi(u)$ be $\istail[\com[u,v],u]$.  Again $\Phi(\NIL)$
is easy to prove by applying the definitions, and assuming $\Phi(u)$ as an
inductive hypothesis, $\Phi(x\.u)$ is
\pskip
$⊗⊗⊗\istail[\com[x\.u,v],x\.u]$\par
$⊗⊗⊗⊗≡\istail[\IF\istail[x\.u,v]\THEN x\.u\ELSE\com[u,v],x\.u]$\par
$⊗⊗⊗⊗≡\IF\istail[x\.u,v]\THEN\istail[x\.u,x\.u]\ELSE\istail[\com[u,v],x\.u]$\par
\pskip
If $\istail[x\.u,v]$ holds, then this becomes true since $\istail[x\.u,x\.u]$.
Otherwise, we get
\pskip
$⊗⊗⊗\istail[\com[u,v],x\.u]$\par
$⊗⊗⊗⊗≡\com[u,v]=x\.u\OR[\NOT\N[x\.u]\AND\istail[\com[u,v],u]]$\par
\pskip
which becomes true by using the inductive hypothesis.

\ppskip
\prob{1.4}. This turned out to be one of the hardest problems.  Here is a fairly
simple proof.  First, some lemmas.
\pskip
\noindent {\bf Lemma 1:}\quad $∀u.\,\istail[\NIL,u]$.
\Proof: Straightforward induction on $u$.
\pskip
\noindent {\bf Lemma 2:}\quad (a) $∀u.\,\com[\NIL,u]=\NIL$.\par
$⊗⊗$(b) $∀u.,\com[u,\NIL]=\NIL$.\par
\Proof: (a) Simple consequence of Lemma 1 and definition of |commontail|.\par
$⊗⊗$(b) Induction on $u$.
\pskip
\noindent {\bf Lemma 3:}\quad
$∀u\,v.\,\istail[u,v]⊃\length u≤\length v$.\par
\Proof: Let $\Phi(v)$ be $∀u.\,\istail[u,v]⊃\length u≤\length v$.
$\Phi(\NIL)$ simplifies to $∀u.\,\istail[u,\NIL]⊃\length u≤0$, and
$\istail[u,\NIL]$ simplifies to $u=\NIL$.  Therefore $\Phi(\NIL)$ is valid.
Assuming $\NOT\N v$ and $\Phi(\D v)$, $\Phi(v)$ becomes
$∀u.\,u=v\OR\istail[u,\D v]⊃\length u≤\length v$.  The case $u=v$ reduces
to true immediately, and the case $\istail[u,\D v]$ implies
$\length u≤\length \D v$, from which $\length u≤\length v$ follows
easily.  This completes the inductive step, and the proof of this lemma.
\pskip
Lemma 3 is used here only to prove Lemma 4,
but could be used much more in a completely different approach to
this set of problems.
\pskip
\noindent {\bf Lemma 4:}\quad $∀u\,v.\,\istail[u,v]\AND\istail[v,u]⊃u=v$.
\Proof: If $u=v$, the implication follows immediately.  So assume $u≠v$.
If $u=\NIL$ and $v≠\NIL$ then $\istail[v,u]$ is false, and we are done.
Similarly if $v=\NIL$ and $u≠\NIL$ then $\istail[u,v]$ must be false.
Finally, if $u≠\NIL$ and $v≠\NIL$, and if $\istail[u,v]\AND\istail[v,u]$,
then both $\istail[u,\D v]$ and $\istail[v,\D u]$ are true from the
definition of |istail|, because $u≠v$.  By
the previous lemma, this means that $\length u≤\length \D v$ and
$\length v≤\length \D u$.  But then it is easy to show that
$\length u<\length v$ and $\length v<\length u$, which contradicts
axioms about the natural numbers, so the left side of the implication must
be false.  Since we have now taken care of all possible cases involving
$u$ and $v$, we can insert the $∀u\,v$ quantifier, and the lemma is proved.
\pskip
Finally, we come to the proof of the main result.
\pskip
\Theorem: $∀u\,v.\,\com[u,v]=\com[v,u]$.
\Proof: The trick is to prove the following formula:
$$∀u\,v\,w.\,\istail[w,u]\AND\istail[w,v]⊃\istail[w,\com[u,v]].$$
This expresses the fact that the |commontail| of $u$ and $v$ is the largest
list that is a tail of both $u$ and $v$.  Now, we prove this formula by
induction on $u$.  $\Phi(\NIL)$ is easy, as usual, because the right side
of the implication simplifies to true using Lemmas 1 and 2.
Assuming $\Phi(u)$, we can write out $\Phi(x\.u)$ as
\pskip
$⊗⊗⊗∀v\,w.\,\istail[w,x\.u]\AND\istail[w,v]⊃\istail[w,\com[x\.u,v]]$\par
$⊗⊗⊗⊗≡∀v\,w.\,\IF\istail[x\.u,v]\THEN\istail[w,x\.u]\AND\istail[w,v]⊃\istail[w,x\.u]$\par
$⊗⊗⊗⊗⊗\ELSE\istail[w,x\.u]\AND\istail[w,v]⊃\istail[w,\com[u,v]]$\par
$⊗⊗⊗⊗≡∀v\,w.\,\NOT\istail[x\.u,v]\AND\istail[w,x\.u]\AND\istail[w,v]⊃\null$\par
$⊗⊗⊗⊗⊗⊗⊗\istail[w,\com[u,v]]$\par
\pskip
In the last line above, the $\THEN$ part of the conditional was seen to be
true from the condition, so the expression could be simplified.  Now,
$\istail[w,x\.u]$ allows us to split into the two cases $w=x\.u$ and
$\istail[w,u]$.  In the first case, $\istail[w,v]$ becomes $\istail[x\.u,v]$,
but we already have the negation of this as part of the same conjunction,
so the left side of the implication is false.  Otherwise, from $\istail[w,u]$
and $\istail[w,v]$, we can derive $\istail[w,\com[u,v]]$ by the inductive
hypothesis, so we are done.  Thus the inductive step is complete.
\pskip
Finally, we use the fact just proved with $w=\com[v,u]$.  Then
$\istail[w,u]$ and $\istail[w,v]$ are the statements proved in problems 1.2
and 1.3, so we can deduce $\istail[w,\com[u,v]]$, that is,
$\istail[\com[v,u],\com[u,v]]$.  By an argument symmetric to the one just
given, we can show that $\istail[\com[u,v],\com[v,u]]$.  Then, applying
Lemma 4, we get the desired final result.

\ppskip
\prob {1.5}. [The following solution is by Oliver Buckley.]  First, define
\pskip
$⊗⊗⊗\upto[u,v]←\IF u=v\THEN\NIL\ELSE\A v\.\upto[u,\D v]$.\par
\pskip
\Lemma: $∀u\,v.\,\istail[u,v]⊃\upto[u,v]*u=v$.
\Proof: Let $\Phi(v)$ be $∀u.\,\istail[u,v]⊃\upto[u,v]*u=v$.  Then $\Phi(\NIL)$
is $∀u.\,\istail(u,\NIL)⊃\upto[u,\NIL]*u=\NIL$.  Now, if $\istail[u,\NIL]$ then
we must have $u=\NIL$ in order to satisfy the definition of |istail|.  Then
$\upto[u,\NIL]*u=\NIL$ is true by applying the definition of |upto|.  For the
inductive step, assume $\Phi(v)$; then $\Phi(x\.v)$ is
$∀u.\,\istail[u,x\.v]⊃\upto[u,x\.v]*u=x\.v$.  There are two cases: $u=x\.v$
or $u≠x\.v$.  If $u=x\.v$, the formula is made true by simplifying and applying
definitions.  Otherwise, it becomes $\istail[u,v]⊃x\.\upto[u,v]*u=x\.v$.
Using the inductive hypothesis, is $\istail[u,v]$, then $\upto[u,v]*u=v$, so
the right side of the implication becomes $x\.v=x\.v$, and the formula is
proved.
\pskip
From this Lemma and problem 1.2, the statement of problem 1.5 follows
immediately.

\ppskip
\prob{1.6}.  This follows immediately from the Lemma above and problem 1.3.
\ppskip

\prob{2.1}.  First we have to write the functions |get| and |point|.
The following definitions are one possibility.
\pskip
$⊗⊗⊗\get[y,p]←$\par
$⊗⊗⊗⊗\IF\N p\THEN y$\par
$⊗⊗⊗⊗\ELSE\IF\A p=\quote{A}\THEN\get[\A y,\D p]$\par
$⊗⊗⊗⊗\ELSE\get[\D y,\D p]$\par
\pskip
$⊗⊗⊗\point[x,y]←$\par
$⊗⊗⊗⊗\IF x=y\THEN\NIL$\par
$⊗⊗⊗⊗\ELSE\IF\AT y\THEN\quote{ERROR}$\par
$⊗⊗⊗⊗\ELSE\IF\point[x,\A y]≠\quote{ERROR}\THEN\quote{A}\.\point[x,\A y]$\par
$⊗⊗⊗⊗\ELSE\IF\point[x,\D y]≠\quote{ERROR}\THEN\quote{D}\.\point[x,\D y]$\par
$⊗⊗⊗⊗\ELSE\quote{ERROR}$\par
\pskip
Notice that |get| does not check the validity of its input, i.e. $p$
might contain members other than {\tt A} or {\tt D}, but anything other
than {\tt A} is treated as if it were {\tt D}.  The |point| function,
on the other hand, returns an error value if its first argument is not
a subexpression of its second argument.  In this case, it also uses this
error value to see whether a recursive call of itself succeeded; a way
to avoid this is to test $|occur|[x,\A y]$ instead of
$\point[x,\A y]≠\quote{ERROR}$, but the result is the same.
\pskip
The problem as it stands is in error, because it only holds for $x$ and
$y$ when $x$ is a subexpression of $y$.  So we will prove
$∀y.\,\Phi(y)$, where $\Phi(y)$ is $∀x.\,\point[x,y]≠\quote{ERROR}⊃
\get[y,\point[x,y]]=x$.  This will be done by S-expression induction.
First, if $y$ is an atom, then from $\point[x,y]≠\quote{ERROR}$ we must
have $x=y$.  But then $\get[y,\point[x,y]]=\get[y,\NIL]=y=x$ and we
have what we want.
\pskip
For the inductive step, we assume $\Phi(y)$ and $\Phi(z)$, and we want
to prove $\Phi(y\.z)$.  Keeping $x$ temporarily fixed, either
$\point[x,y\.z]=\quote{ERROR}$, in which case we are done, or
$\point[x,y\.z]≠\quote{ERROR}$.  Then, if $x=y\.z$, we have
$\get[y\.z,\point[x,y\.z]]=\get[y\.z,\NIL]=y\.z=x$; and if $x≠y\.z$, then
\pskip
$⊗⊗⊗\get[y\.z,\point[x,y\.z]]$\par
$⊗⊗⊗⊗=\get[y\.z,\IF\point[x,y]≠\quote{ERROR}\THEN\quote{A}\.\point[x,y]$\par
$⊗⊗⊗⊗⊗⊗\quad\ELSE\IF\point[x,z]≠\quote{ERROR}\THEN\quote{D}\.\point[x,z]$\par
$⊗⊗⊗⊗⊗⊗\quad\ELSE\quote{ERROR}]$\par
$⊗⊗⊗⊗=\IF\point[x,y]≠\quote{ERROR}\THEN\get[y\.z,\quote{A}\.\point[x,y]]$\par
$⊗⊗⊗⊗\quad\ELSE\IF\point[x,z]≠\quote{ERROR}\THEN\get[y\.z,\quote{D}\.\point[x,z]]$\par
$⊗⊗⊗⊗\quad\ELSE\get[y\.z,\quote{ERROR}]$\par
\pskip
The last case of the conditional cannot occur, since it contradicts
$\point[x,y\.z]≠\quote{ERROR}$, which we are assuming.  Applying the definition
of |get| to the other case and using the inductive hypotheses, we get $x$
in both of the first two cases.  Therefore, $\get[y\.z,\point[x,y\.z]]=x$.
We now quantify over $x$, since no special assumptions were made about it,
and this completes the inductive step of the proof.

\vfill\end